Metamath Blueprint : Derivative of real logarithm (iset)

This is a quick summary of what is needed to intuitionize dvrelog.

---